/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.api;

import alloy.ast.Node;
import alloy.util.SetOfLong;

/**
 * An interface representing an unsatisfiable core of the lifted (quantified,
 * i.e. not ground-out) translatable AST.  We actually compute a more precise
 * unsatisfiable core -- on the ground-out AST; so e.g. if you have a constraint
 * "all x: A | F(x)", which grounds out to "F({<A_0>}) && F({<A_1>}) F({<A_2>})",
 * we may determine that only F({<A_0>}) belongs to the core.  But for the sake
 * of simpler interface, here we'll say that the entire lifted formula
 * "all x: A | F(x)" belongs to the core.
 * 
 * @see AlloyRunner#computeLiftedUnsatCore for the only implementation of this interface
 */
public interface LiftedUnsatCore {
    /**
     * Tell whether a given node of the translatable AST belongs to the unsatisfiable core.
     * If a node is not in the core, the function it computes of its children may be changed
     * arbitrarily without making the AST satisfiable.
     * 
     * @param node_
     */
    public boolean isInCore(Node node_);

    /**
     * @param node_ a node in the lifted AST
     * @return an ArrayList of the templateID's that represent that node's Boolean formula
     */
	public SetOfLong nodeTemplates(Node node_);
}


